Nuprl Lemma : no_repeats-insert
0,22
postcript
pdf
T
:Type,
eq
:EqDecider(
T
),
a
:
T
,
L
:
T
List. no_repeats(
T
;
L
)
no_repeats(
T
;insert(
a
;
L
))
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
P
&
Q
,
t
T
,
no_repeats(
T
;
l
)
,
EqDecider(
T
)
Lemmas
insert
property
,
deq
wf
origin
T:Type, eq:EqDecider(T), a:T, L:T List. no_repeats(T;L) 
no_repeats(T;insert(a;L)) T:Type, eq:EqDecider(T), a:T, L:T List. no_repeats(T;L) no_repeats(T;insert(a;L)) x:A. B(x) Q
T